The one-page cheat sheet.wiki (2048B)
1 == One-page cheat sheet == 2 === Definitions === 3 * Model is: 4 * set A - domain 5 * interpretation operation for predicate and function symbols 6 * satisfiable: some model & environment where it's true 7 * valid: true in all models and environments 8 * derivable: can be proven without global hypothesis 9 * tautology: true under any truth assignment (valid) 10 * soundness: ⊢ A → ⊨ A (from syntax to semantics) 11 * completeness: ⊨ A → ⊢ A (from semantics to syntax) 12 * partial order: antisymmetric, reflexive, transitive 13 * memo technique -- p**art**ial means **a**ntisymmetric, **r**eflexive, **t**ransitive 14 * strict means irreflexive 15 * total order: partial order & ∀ ab: R(a,b) ∨ R(b,a) 16 * strict: ∀ ab: R(a,b) ∨ a = b ∨ R(b,a) 17 * equivalence relation: has all three properties in the positive (symmetric, reflexive, transitive) 18 19 environment is used to interpret free variables 20 === Modal logic === 21 * □ Φ: true in world if true in all related worlds (if no related, true). 22 * ◇ Φ: true in world if true in some related world (if no related, false). 23 24 M,w ⊩ Φ: Φ true in world w of Kripke model M (true in model if true in every world) 25 26 Φ valid in frame if true with every labelling. 27 28 frame = Kripke - labels 29 30 === Metatheorems === 31 * consistent: has a model 32 * syntactically consistent: can't derive ⊥ 33 * compactness: if Γ is consistent, every finite subset of Γ is also consistent 34 35 === Definability === 36 Model finiteness is undefinable. 37 38 Model infiniteness is definable by a set of formulas. 39 40 In predicate logic, only unreachability by n steps is definable, and only by a set of sentences. 41 42 === Decidability === 43 Y ⊆ I decidable if program can tell for every i ∈ I whether i ∈ Y. I set, Y predicate on set. 44 45 Undecidable: termination, PCP, validity, provability, satisfiability. 46 47 Termination can be reduced to PCP, which can be reduced to validity. 48 49 Incompleteness theorems: every non-trivial formal system is 50 * either incomplete (valid but not derivable) 51 * or inconsistent (doesn't have a model, or entails ⊥) 52